dependent type theory #type_theory #incomplete type References https://ncatlab.org/nlab/show/dependent+type+theory